ma-prob-da-dom(M;b)
== ((b  dom((M.2.2.2.2.2.2.2.2.2.2.2).1))  (locl(b)  dom((M.2).1)))
== & (b in dom(M.pre)  (b  dom(M.prob))) 

latex

---

clarification:

ma-prob-da-dom(M;b)
== ((fpf-dom(IdDeq; b; ((M.2.2.2.2.2.2.2.2.2.2.2).1)))  (fpf-dom(KindDeq; locl(b); ((M.2).1))))
== & (b in dom(M.pre)  (b  dom(M.prob))) 

latex

Definitions	P & Q, IdDeq, x  dom(f), KindDeq, locl(a), t.1, t.2, P  Q, a in dom(M.pre), b, b  dom(M.prob)
FDL editor aliases	ma-prob-da-dom